Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

More details in the documentation of native arrays #13125

Merged
merged 1 commit into from Oct 2, 2020
Merged

More details in the documentation of native arrays #13125

merged 1 commit into from Oct 2, 2020

Conversation

VincentSe
Copy link
Contributor

Kind: documentation.

@VincentSe VincentSe requested a review from a team as a code owner October 1, 2020 16:41
jfehrle
jfehrle reviewed Oct 1, 2020
View reviewed changes
Copy link
Member

@jfehrle jfehrle left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Some suggestions.

doc/sphinx/language/core/primitive.rst Outdated Show resolved Hide resolved
doc/sphinx/language/core/primitive.rst Outdated Show resolved Hide resolved
doc/sphinx/language/core/primitive.rst Outdated Show resolved Hide resolved
@VincentSe VincentSe force-pushed the DocNativeArrays branch 3 times, most recently from ba75879 to ab41b88 Compare October 2, 2020 08:19
herbelin
herbelin reviewed Oct 2, 2020
View reviewed changes
Copy link
Member

@herbelin herbelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks a lot for clarifying this part of the documentation.

doc/sphinx/language/core/primitive.rst Outdated Show resolved Hide resolved
jfehrle
jfehrle approved these changes Oct 2, 2020
View reviewed changes
Copy link
Member

@jfehrle jfehrle left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

A few small wording suggestions. Also, would you squash the two commits? Let me know when you're done and I will merge.

doc/sphinx/language/core/primitive.rst Outdated Show resolved Hide resolved
doc/sphinx/language/core/primitive.rst Outdated Show resolved Hide resolved
@jfehrle jfehrle self-assigned this Oct 2, 2020
@jfehrle jfehrle modified the milestones: 8.13+beta1, 8.12.2 Oct 2, 2020
@jfehrle jfehrle added the kind: documentation Additions or improvement to documentation. label Oct 2, 2020
@VincentSe @jfehrle
More details in the documentation of native arrays
1347abe 
Update doc/sphinx/language/core/primitive.rst

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

Add persistent data structure

Update doc/sphinx/language/core/primitive.rst

Co-authored-by: Hugo Herbelin <herbelin@users.noreply.github.com>

Update doc/sphinx/language/core/primitive.rst

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

Update doc/sphinx/language/core/primitive.rst

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
@VincentSe
Copy link
Contributor Author

@jfehrle The commits are squashed. Thanks

@jfehrle
Copy link
Member

jfehrle commented Oct 2, 2020

Thanks for the PR!

@coqbot: merge now

@coqbot-app coqbot-app bot merged commit 706ec6e into coq:master Oct 2, 2020
@VincentSe VincentSe deleted the DocNativeArrays branch October 3, 2020 07:47
@Zimmi48 Zimmi48 modified the milestones: 8.12.2, 8.12.1 Oct 8, 2020
@Zimmi48 Zimmi48 added this to Request 8.12.1 inclusion in Coq 8.12 Oct 8, 2020
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Oct 8, 2020

This PR was postponed. Please update accordingly the milestone of any issue that this fixes as this cannot be done automatically.

@Zimmi48 Zimmi48 removed this from Request 8.12.1 inclusion in Coq 8.12 Oct 8, 2020
@coqbot-app coqbot-app bot modified the milestones: 8.12.1, 8.13+beta1 Oct 8, 2020
@Zimmi48
Copy link
Member

Zimmi48 commented Oct 8, 2020

(Primitive arrays were introduced in 8.13.)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Blaisorblade Blaisorblade Blaisorblade left review comments

@herbelin herbelin herbelin left review comments

@jfehrle jfehrle jfehrle approved these changes

Assignees

@jfehrle jfehrle

Labels
kind: documentation Additions or improvement to documentation.
Projects
None yet
Milestone
8.13+beta1
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@VincentSe @jfehrle @Zimmi48 @Blaisorblade @herbelin